package dv;
import dv.apkeep.Model;
import dv.network.Device;
import dv.network.Network;
import dv.network.Port;
import dv.network.Rule;

import java.io.File;
import java.io.FileNotFoundException;
import java.math.BigInteger;
import java.util.ArrayList;
import java.util.HashSet;
import java.util.Scanner;

public class Test {
    public static void main(String[] args) {
        Network n = new Network();
        String[] devicenames = {"atla", "chic", "hous", "kans", "losa", "newy32aoa", "salt", "seat", "wash"};

        // add a default device for blackholes, since dfg need a peer node for default port of each device
        n.addDevice("default");
        for (String name : devicenames) {
            n.addDevice(name);
            n.addLink(name, "default", "default", name + "-peer-default");
        }
        n.addLink("chic", "xe-0/1/0", "newy32aoa", "xe-0/1/3");
        n.addLink("chic", "xe-1/0/1", "kans", "xe-0/1/0");
        n.addLink("chic", "xe-1/1/3", "wash", "xe-6/3/0");
        n.addLink("hous", "xe-3/1/0", "losa", "ge-6/0/0");
        n.addLink("kans", "ge-6/0/0", "salt", "ge-6/1/0");
        n.addLink("chic", "xe-1/1/2", "atla", "xe-0/1/3");
        n.addLink("seat", "xe-0/0/0", "salt", "xe-0/1/1");
        n.addLink("chic", "xe-1/0/2", "kans", "xe-0/0/3");
        n.addLink("hous", "xe-1/1/0", "kans", "xe-1/0/0");
        n.addLink("seat", "xe-0/1/0", "losa", "xe-0/0/0");
        n.addLink("salt", "xe-0/0/1", "losa", "xe-0/1/3");
        n.addLink("seat", "xe-1/0/0", "salt", "xe-0/1/3");
        n.addLink("newy32aoa", "et-3/0/0-0", "wash", "et-3/0/0-0");
        n.addLink("newy32aoa", "et-3/0/0-1", "wash", "et-3/0/0-1");
        n.addLink("chic", "xe-1/1/1", "atla", "xe-0/0/0");
        n.addLink("losa", "xe-0/1/0", "seat", "xe-2/1/0");
        n.addLink("hous", "xe-0/1/0", "losa", "ge-6/1/0");
        n.addLink("atla", "xe-0/0/3", "wash", "xe-1/1/3");
        n.addLink("hous", "xe-3/1/0", "kans", "ge-6/2/0");
        n.addLink("atla", "ge-6/0/0", "hous", "xe-0/0/0");
        n.addLink("chic", "xe-1/0/3", "kans", "xe-1/0/3");
        n.addLink("losa", "xe-0/0/3", "salt", "xe-0/1/0");
        n.addLink("atla", "ge-6/1/0", "hous", "xe-1/0/0");
        n.addLink("atla", "xe-1/0/3", "wash", "xe-0/0/0");
        n.addLink("chic", "xe-2/1/3", "wash", "xe-0/1/3");
        n.addLink("atla", "xe-1/0/1", "wash", "xe-0/0/3");
        n.addLink("kans", "xe-0/1/1", "salt", "ge-6/0/0");
        n.addLink("chic", "xe-1/1/0", "newy32aoa", "xe-0/0/0");

        // step2: build the network model for verifier
        Model model = new Model(n);
        n.setModel(model);

        // step3: add default rules to devices as apkeep need default rules before any updates
        for (Device device : n.getDevices().values()) {
            Port defaultPort = device.addPortByName(device.getName() + "-default");
            Rule rule = new Rule(BigInteger.valueOf(0), 0, defaultPort);
            n.addRule(device, rule);
            model.portToPreds.put(defaultPort, new HashSet<>());
            model.portToPreds.get(defaultPort).add(1);
            model.predToPorts.get(1).add(defaultPort);
        }

        // step4: add rules and do verification
        for (String name : devicenames) {
            File inputFile = new File("i2/" + name + "apnotcomp");
            Scanner line = null;
            try {
                line = new Scanner(inputFile);
                line.useDelimiter("\n");
            } catch (FileNotFoundException e) {
                e.printStackTrace();
                System.exit(0);
            }

            while (line.hasNext()) {
                String linestr = line.next();
                String[] tokens = linestr.split(" ");
                if (tokens[0].equals("fw")) {
                    String portname = tokens[3].split("\\.")[0];
                    Port p = n.getDevices().get(name).getPortByName(portname);
                    if (p == null) {
                        p = n.getDevices().get(name).addPortByName(portname);
                    }
                    Rule rule = new Rule(BigInteger.valueOf(Long.parseLong(tokens[1])), Integer.parseInt(tokens[2]), p);

                    // this function will update PPM and check invariants
                    n.addRule(n.getDevices().get(name), rule);
                }
            }
        }

        System.out.println("total #ecs: " + model.predToPorts.size());
    }
}
